/*Z
内核虚拟地址空间，从高至低：
    大小    符号            用途
------------------------------------
    1G      KDEV_BASE       设备
    1G      KERNEL_BASE     代码
    512-2G  PPTR_BASE       内核窗口（好像是为了一一映射物理内存）

*/

/*
 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
 *
 * SPDX-License-Identifier: GPL-2.0-only
 */

#pragma once

#include <util.h>

/*
 *          2^64 +-------------------+
 *               | Kernel Page PDPT  | --+
 *   2^64 - 2^39 +-------------------+ PPTR_BASE
 *               |    TLB Bitmaps    |   |
 *               +-------------------+   |
 *               |                   |   |
 *               |     Unmapped      |   |
 *               |                   |   |
 *   2^64 - 2^47 +-------------------+   |
 *               |                   |   |
 *               |   Unaddressable   |   |
 *               |                   |   |
 *          2^47 +-------------------+ USER_TOP
 *               |                   |   |
 *               |       User        |   |
 *               |                   |   |
 *           0x0 +-------------------+   |
 *                                       |
 *                         +-------------+
 *                         |
 *                         v
 *          2^64 +-------------------+
 *               |                   |
 *               |                   |     +------+     +------+
 *               |  Kernel Devices   | --> |  PD  | --> |  PT  |
 *               |                   |     +------+     +------+
 *               |                   |
 *   2^64 - 2^30 +-------------------+ KDEV_BASE
 *               |                   |
 *               |                   |     +------+
 *               |    Kernel ELF     | --> |  PD  |
 *               |                   |     +------+
 *               |                   |
 *   2^64 - 2^29 +-------------------+ PPTR_TOP / KERNEL_ELF_BASE
 *               |                   |
 *               |  Physical Memory  |
 *               |       Window      |
 *               |                   |
 *   2^64 - 2^39 +-------------------+ PPTR_BASE
 */

/* WARNING: some of these constants are also defined in linker.lds
 * These constants are written out in full instead of using bit arithmetic
 * because they need to defined like this in linker.lds
 */
/*Z 用户空间上限。避免x86_64第47位地址位要规范化符号扩展问题，同时因为线程最后至少有IPC buffer，因此没有指令能使cpu预取地址超限 */
/* Define USER_TOP to be 1 before the last address before sign extension occurs.
 * This ensures that
 *  1. user addresses never needed to be sign extended to be valid canonical addresses
 *  2. the user cannot map the last page before addresses need sign extension. This prevents
 *     the user doing a syscall as the very last instruction and the CPU calculated PC + 2
 *     from being an invalid (non sign extended) address
 */
#define USER_TOP UL_CONST(0x7FFFFFFFFFFF)

/* The first physical address to map into the kernel's physical memory
 * window */
#define PADDR_BASE UL_CONST(0x00000000)
/*Z 内核虚拟地址空间基地址。48位空间中的顶端512G */
/* The base address in virtual memory to use for the 1:1 physical memory
 * mapping. Our kernel window is 2^39 bits (2^9 * 1gb) and the virtual
 * address range is 48 bits. Therefore our base is 2^48 - 2^39 */
#define PPTR_BASE UL_CONST(0xffffff8000000000)
/*Z seL4利用一级页表的倒数几项（除最后一项），记录当前TLB对应的cpu id，一项可以表示63个cpu(位0恒0)，占用512G的虚拟地址空间 */
/* Below the main kernel window we have any slots for the TLB bitmap */
#define TLBBITMAP_PML4_RESERVED (TLBBITMAP_ROOT_ENTRIES * BIT(PML4_INDEX_OFFSET))
#define TLBBITMAP_PPTR (PPTR_BASE - TLBBITMAP_PML4_RESERVED)
/*Z 内核代码虚拟基地址。虚拟地址空间的顶端2G */
/* The kernel binary itself is placed in the bottom 1gb of the top
 * 2gb of virtual address space. This is so we can use the 'kernel'
 * memory model of GCC, which requires all symbols to be linked
 * within the top 2GiB of memory. This is (2^48 - 2 ^ 31) */
#define PPTR_TOP UL_CONST(0xffffffff80000000)

/* The physical memory address to use for mapping the kernel ELF */
#define KERNEL_ELF_PADDR_BASE UL_CONST(0x00100000)

/* Kernel mapping starts directly after the physical memory window */
#define KERNEL_ELF_BASE (PPTR_TOP + KERNEL_ELF_PADDR_BASE)
/*Z 内核设备虚拟基地址。虚拟地址空间的顶端1G */
/* Put the kernel devices at the very beginning of the top
 * 1GB. This means they are precisely after the kernel binary
 * region. This is 2^48 - 2^30 */
#define KDEV_BASE UL_CONST(0xffffffffc0000000)

#ifndef __ASSEMBLER__

#include <config.h>
#include <basic_types.h>
#include <plat/machine.h>
#include <plat_mode/machine/hardware_gen.h>
#include <arch/kernel/tlb_bitmap_defs.h>

/* ensure the user top and tlb bitmap do not overlap if multicore */
#ifdef ENABLE_SMP_SUPPORT
compile_assert(user_top_tlbbitmap_no_overlap, GET_PML4_INDEX(USER_TOP) != GET_PML4_INDEX(TLBBITMAP_PPTR))
#endif

/* since we have two kernel VM windows, we have two pptr to paddr
 * conversion functions.
 * paddr_to_kpptr converts physical address to the second small kernel
 * window which locates at the top 2GiB.
 */
static inline void *CONST
paddr_to_kpptr(paddr_t paddr)
{
    assert(paddr < KERNEL_ELF_PADDR_TOP);
    return (void *)(paddr + KERNEL_ELF_BASE_OFFSET);
}
/*Z 内核虚拟地址转换为物理地址：减KERNEL_BASE_OFFSET */
static inline paddr_t CONST kpptr_to_paddr(void *pptr)
{
    assert((word_t)pptr >= KERNEL_ELF_BASE);
    return (paddr_t)pptr - KERNEL_ELF_BASE_OFFSET;
}

#endif /* __ASSEMBLER__ */

